(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
fst(0, Z) → nil
fst(s, cons(Y)) → cons(Y)
from(X) → cons(X)
add(0, X) → X
add(s, Y) → s
len(nil) → 0
len(cons(X)) → s
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
fst(0, z0) → nil
fst(s, cons(z0)) → cons(z0)
from(z0) → cons(z0)
add(0, z0) → z0
add(s, z0) → s
len(nil) → 0
len(cons(z0)) → s
Tuples:
FST(0, z0) → c
FST(s, cons(z0)) → c1
FROM(z0) → c2
ADD(0, z0) → c3
ADD(s, z0) → c4
LEN(nil) → c5
LEN(cons(z0)) → c6
S tuples:
FST(0, z0) → c
FST(s, cons(z0)) → c1
FROM(z0) → c2
ADD(0, z0) → c3
ADD(s, z0) → c4
LEN(nil) → c5
LEN(cons(z0)) → c6
K tuples:none
Defined Rule Symbols:
fst, from, add, len
Defined Pair Symbols:
FST, FROM, ADD, LEN
Compound Symbols:
c, c1, c2, c3, c4, c5, c6
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 7 trailing nodes:
LEN(cons(z0)) → c6
FST(0, z0) → c
FST(s, cons(z0)) → c1
ADD(s, z0) → c4
FROM(z0) → c2
LEN(nil) → c5
ADD(0, z0) → c3
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
fst(0, z0) → nil
fst(s, cons(z0)) → cons(z0)
from(z0) → cons(z0)
add(0, z0) → z0
add(s, z0) → s
len(nil) → 0
len(cons(z0)) → s
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
fst, from, add, len
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(6) BOUNDS(1, 1)